# To change this template, choose Tools | Templates
# and open the template in the editor.
$LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../../..','ext_pr1/lib')
require 'ext_pr1_v4'

class Object
 def graph_obj?() point? or prim_shape? or union_shape? end
  def point?() false end
  def shape?() false end
  def shape1d?() false end
  def shape2d?() false end
  def prim_shape?() false end
  def union_shape?() false end
  def point1d?() false end
  def range1d?() false end
  def union1d?() false end
  def point2d?() false end
  def range2d?() false end
  def union2d?() false end
end
class Integer
  def include1dim?(first, last)
    ((first <= self) and (self <= last))
  end
  
end

   class GraphObj
     def graph_obj?() true end
     def invariant() abstract end
     def graph_equal?(o2) abstract end
     def graph_equal_trans?(o2) abstract end
   end 
   
   
   class Point < GraphObj
     
     def point?() true end
   end
   
   class Shape < GraphObj
     def to_s() abstract end
     def graph_equal() abstract end
     def ==() abstract end
     def shape?() true end
     
     
     
   end    
   
class Union < Shape
       def point?() false end
       def shape?() true end
       def prim_shape?() false end
       def union_shape?() true end
  
      #allgemeine prüfung auf gleichheit
      #Union#graph_equal? ::= o1,o2 :: Shape x Shape ->? Bool

      def graph_equal?(o2)
      check_pre((o2.graph_obj?()))
      self.graph_equal_?(o2)
      end
  
      #bounding range einer beliebigen shape
      #Union#bounds ::= shape :: Shape -> Range1d|Range2d
      def bounds()
          self.left.bounds().bounding_range(self.right.bounds())
      end
end
   
class Ranges < Shape
   def prim_shape?() true end
   
   #bounding range einer beliebigen shape
   #Range#bounds ::= shape :: Shape -> Range1d|Range2d   
    def bounds()
      self 
    end

   #prüft, ob ein Punkt in einer Shape enthalten ist
   #Range1d#in? ::= shape,point :: Shape x Point -> Bool
   def in?(point)
    check_pre((point.point1d?))
    point.include?(self)
   end
end
   

#1D KLASSEN

#1 dimensionaler punkt
#def range1d?(range) 
#Point1d ::= :Point1d[:x] :: x = Int
 
class Point1d < Point
  
  def initialize(coord)
    @coord = coord
  end
  #EQUIVALENCIES
   
  def ==(value)
   self.equal?(value) or (self.coord == value.coord)
  end
  #SELECTOR 
  def coord()
    @coord
   end
  
 
  #CONVERSION
  def to_s
    'Point1d'+'['+(self.coord.to_s)+']'
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  

  
  #TYPEPREDS
  def point1d?() true end
  def invariant?()
    coord.int? 
  end
  
  #OPERATIONS
  #translation eines Punktes in einer Dimension
  #Point1d#translate0d ::= p1,p2 :: Point1d x Point1d -> Point1d
  def translate0d(p2)
   check_pre((self.point1d? and p2.point1d?))
   Point1d[(self.coord + p2.coord)]
  end
  #bounding range einer beliebigen shape
  #Point1d#bounds ::= point :: Point -> Err   
    def bounds()
    check_pre((false))
    end
  #prüfung auf gleichheit
  #Point1d#graph_equal ::= o1,o2 :: Point1d x Point1d -> Bool
    def graph_equal_?(o2)
      self.coord == o2.coord
    end
  #allgemeine prüfung auf gleichheit
  #Point1d#graph_equal? ::= o1,o2 :: Point x Point ->? Bool

    def graph_equal?(o2)
     check_pre((o2.graph_obj?()))
     self.graph_equal_?(o2)
  end
  #prüft, ob 2 objekte deckungsgleich sind
  #Point1d#graph_equal_trans? ::= Point x Point ->? Bool
  def graph_equal_trans?(o2)
    check_pre((o2.point1d?))
    to1 = Point1d[o1.coord + (o2.coord - self.coord)]  
    to1.graph_equal?(o2)
  end
  #prüft, ob ein punkt in einem range enthalten ist
  #Point1d#include? ::= point,range :: Point1d x Range1d -> Bool
  def include?(range)
    check_pre((range.range1d?))
    self.coord.include1dim?(range.first.coord, range.last.coord)
  end
  
end
#1 dimensionales intervall mit 1 dimensionalen punkten
#Range1d ::= :Range[:first,:last] :: first, last :: first, last == :Point1d
class Range1d < Ranges
  def initialize(first, last)
    @first = first
    @last = last
  end
    #EQUIVALENCIES
  def ==(value)
   self.equal?(value) or(self.first == value.first and self.last == value.last)
  end
  
  #SELECTORS
  def first()
    @first
  end
  
  def last()
    @last
  end
 
  #CONVERSIONS
  def to_s
    'Range1d'+'['+(self.first.to_s)+','+(self.last.to_s)+']'
  end
 #TYPEPREDS
  def range1d?()
  self == Range1d
  end
    def graph_obj?() true end
  def shape1d?() true end
 
  def range1d?() true end
  
  
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  def invariant?()
    first.point1d? and last.point1d? and  first.coord <= last.coord
  end
 
  #OPERATIONS
 #translatierung eines 1d ranges
 #Range1d#translate1d ::= range,point :: Range1d x Point1d -> Range1d
  def translate1d(point)
  check_pre((point.point1d?))
  Range1d[self.first.translate0d(point), self.last.translate0d(point)]
  end
 #translatierung allgemein
 #Range1d#translate ::= (shape,point) :: Shape x Point ->? Shape
  def translate(point)
  check_pre((point.point?))
  self.translate1d(point)
  end 
#bounding range von 2 ranges gleicher dimension
#Range1d#bounding_range ::= r1,r2 :: Range1d x Range1d -> Range1d
    def bounding_range(r2)
    check_pre((r2.range1d?))
    Range1d[Point1d[self.first.coord.min(r2.first.coord)],Point1d[self.last.coord.max(r2.last.coord)]]
    end

#hilfsfunktion für graph_equal?
 def graph_equal_?(o2)
   (self.first.graph_equal?(o2.first) and self.last.graph_equal?(o2.last))
 end
  #allgemeine prüfung auf gleichheit
  #Range1d#graph_equal? ::= o1,o2 :: Shape x Shape ->? Bool

    def graph_equal?(o2)
     check_pre((o2.graph_obj?()))
     self.graph_equal_?(o2)
     
  end
  #prüft, ob 2 objekte deckungsgleich sind
  #Range1d#graph_equal_trans? ::= Shape x Shape ->? Bool
  def graph_equal_trans?(o2)
  check_pre((o2.shape1d?))
  to1 = self.translate(Point1d[(o2.bounds().first.coord - self.bounds().first.coord)])
   to1.graph_equal?(o2)
  end

  #hilfsfunktion für include?
  def include?(point)
    point.coord.include1dim?(self.first.coord, self.last.coord)
  end
end

#Union1d als Vereinigung von 2 Shape1d
#Union1d ::= :Union1d[:shape1, :shape2] :: shape1, shape2 :: shape1, shape2 == :Shape1d

class Union1d < Union
  def initialize(left, right)
    @left = left
    @right = right
  end
  #EQUIVALENCIES
  def ==(value)
    self.equal?(value) or (self.left == value.left and self.right == value.right)
  end
  
  
  #SELECTORS
  def left()
    @left
  end
  
  def right()
    @right
  end
  
  #CONVERSIONS
  def to_s
    'Union1d'+'['+(self.left.to_s)+','+(self.right.to_s)+']'
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
   def invariant?()
    left.shape1d? and  right.shape1d?
  end
  
  #TYPEPREDS
  def union1d?()
  self == Union1d
  end

  def shape1d?() true end
  def shape2d?() false end

  #OPERATIONS

   #operations 
def translate1d(point)
  check_pre((point.point1d?))
 
 Union1d[self.left.translate1d(point), self.right.translate1d(point)]
  
  end

  
#OPERATIONS
#translatierung allgemein
#Union1d#translate ::= (shape,point) :: Shape x Point ->? Range1d|Range2d
def translate(point)
check_pre((point.point1d?))
self.translate1d(point)
end 

#hilfsfunktion für graph_equal?
def graph_equal_?(o2)
  (self.left.graph_equal?(o2.left) and self.right.graph_equal?(o2.right))
end
#prüft, ob 2 objekte deckungsgleich sind
  #Union1d#graph_equal_trans? ::= Shape x Shape ->? Bool
  def graph_equal_trans?(o2)
    check_pre((o2.shape1d?))
  to1 = self.translate(Point1d[(o2.bounds().first.coord - self.bounds().first.coord)])
   to1.graph_equal?(o2)
  end
#allgemeine prüfung auf gleichheit
#Union1d#graph_equal? ::= o1,o2 :: Shape x Shape ->? Bool

     def graph_equal?(o2)
     check_pre((o2.graph_obj?()))
     self.graph_equal_?(o2)
     
  end
  #prüft, ob ein Punkt in einer Shape enthalten ist
#Union1d#in? ::= shape,point :: Shape x Point -> Bool
      def in?(point)
      check_pre((point.point1d?))
      (point.in?(self.left) or point.in?(self.right))
      end
end
#Shape1d als Überbegriff für Union1d und Range1d
#:Shape1d ::= :Shape1d[:shape] :: shape :: shape == :Range1d or shape == Union1d

#def_class(:Shape1d,[:shape]) {
#  def invariant? 
#    shape1dim?(shape)
#  end 
#}


#2D KLASSEN

#2d punkt als kreuzprodukt aus 2 Point1d
# :Point2d ::= :Point2d[x,y] :: x, y :: x,y == :Point1d

class Point2d < Point

  def initialize(x, y)
    @x = x
    @y = y
  end

    #SELECTORS
 def x; @x end
 def y; @y end

  #EQUIVALENCIES
  def ==(value)
    value.graph_obj? and  ((self.x == value.x) and (self.y == value.y))
  end 

  #TYPEPREDS
  def point2d?()
    true
  end
  def to_s
    'Point2d'+'['+((self.x).to_s)+','+((self.y).to_s)+']'
  end
  
  
  #TYPEPREDS  
  def self.[](*args) check_inv(self.new(*args)) end
  def invariant?()
   x.point1d? and y.point1d?
  end
  #OPERATIONS
  #hilfsfunktion für graph_equal?
  def graph_equal_?(o2)
    
    o2.point2d? and
    (self.x.graph_equal_?(o2.x) and self.y.graph_equal_?(o2.y))
  end
  #allgemeine prüfung auf gleichheit
#Point2d#graph_equal? ::= o1,o2 :: Point x Point ->? Bool

    def graph_equal?(o2)
     check_pre((o2.graph_obj?()))
     self.graph_equal_?(o2)
     
  end
  #prüft, ob 2 objekte deckungsgleich sind
  #Point2d#graph_equal_trans? ::= Point x Point ->? Bool
      def graph_equal_trans?(o2)
    check_pre((o2.point2d?))
    to1 = Point2d[Point1d[self.x.coord + (o2.x.coord - self.x.coord)], Point1d[self.y.coord + (o2.y.coord - self.y.coord)]]
    to1.graph_equal?(o2)
  end
#bounding range einer beliebigen shape
#Point2d#bounds ::= shape :: Shape -> Range1d|Range2d     
  def bounds()
    check_pre((false))
  end
  #prüft, ob ein punkt in einem range enthalten ist
  #Point2d#include? ::= point,range :: Point2d x Range2d -> Bool
  def include?(range)
    (self.x.coord.include1dim?(range.range_x.first.coord, range.range_x.last.coord) and self.y.coord.include1dim?(range.range_y.first.coord, range.range_y.last.coord))
  end
  
end

#2d range als kreuzprodukt aus 2 Range1d
# :Range2d ::= :Range2d[range_x, range_y] :: range_x, range_y :: range_x, range_y == Range1d

class Range2d < Shape
  def initialize(range_x, range_y)
    @range_x = range_x
    @range_y = range_y
  end
    #EQUIVALENCIES
  def ==(value)
    self.equal?(value) or (self.range_x == value.range_x and self.range_y == value.range_y)
  end

  #SELECTORS
  def range_x()
    @range_x
  end
  
  def range_y()
    @range_y
  end
    def range2d?()
  self == Range2d
  end

  #CONVERSIONS
  def to_s
    'Range2d'+'['+(self.range_x.to_s)+','+(self.range_y.to_s)+']'
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  def invariant?
    range_x.range1d? and range_y.range1d?
  end
 
 
  #TYPEPREDS
    def graph_obj?() true end
  def point?() false end
  def shape?() true end
  def shape1d?() false end
  def shape2d?() true end
  def prim_shape?() true end
  def union_shape?() false end

  
  #OPERATIONS
  
   #translatierung einer 2d shape
 #Range2d#translate2d ::= shape,point :: Shape2d x Point2d -> Shape2d
  def translate2d(point)
    check_pre((point.point2d?))
    Range2d[self.range_x.translate1d(point.x), self.range_y.translate1d(point.y)]
  end
  #translatierung allgemein
#Range2d#translate ::= (shape,point) :: Shape x Point ->? Range1d|Range2d
def translate(point)
check_pre((point.point2d?))
self.translate2d(point)
end 

 #bounding range von 2 2d ranges
 #Range2d#bounding_range ::= r1,r2 :: Range2d x Range2d -> Range2d
def bounding_range(r2)
 Range2d[self.range_x.bounding_range(r2.range_x),self.range_y.bounding_range(r2.range_y)]
    end
#bounding range einer beliebigen shape
#Range2d#bounds ::= shape :: Shape -> Range1d|Range2d    
 def bounds()
self
end
#hilfsfunktion für graph_equal?
def graph_equal_?(o2)
 (self.range_x.graph_equal?(o2.range_x) and self.range_y.graph_equal?(o2.range_y)) 
end

#allgemeine prüfung auf gleichheit
#Range2d#graph_equal? ::= o1,o2 :: Shape x Shape ->? Bool
     def graph_equal?(o2)
     check_pre((o2.graph_obj?()))
     self.graph_equal_?(o2)
     
  end
  #prüft, ob 2 objekte deckungsgleich sind
  #Range2d#graph_equal_trans? ::= Shape x Point ->? Bool
       def graph_equal_trans?(o2)
    check_pre((o2.shape2d?))
   to1 = self.translate(Point2d[Point1d[(o2.bounds().range_x.first.coord - self.bounds().range_x.first.coord)], Point1d[(o2.bounds().range_y.first.coord - self.bounds().range_y.first.coord)]])   
   to1.graph_equal?(o2)
  end
  #prüft, ob ein Punkt in einer Shape enthalten ist
#Range2d#in? ::= shape,point :: Shape x Point -> Bool
   def in?(point)
    check_pre((point.point2d?))
    point.include?(self)
  end

 #hilfsfunktion für include?
 def include?(point)
   check_pre((point.point?))
   point.x.coord.include1dim?(self.range_x.first.coord,self.range_x.last.coord ) and 
   point.y.coord.include1dim?(self.range_y.first.coord,self.range_y.last.coord )
 end
end
#2d union als vereinigung von 2 shapes
# :Union2d ::= :Union[:left,:right] :: left, right :: left, right == Shape2d

class Union2d < Union
    
  #EQUIVALENCIES
  def ==(value)
   self.equal?(value) or (self.left == value.left and self.right == value.right)
  end
  
  
    def initialize(left, right)
    @left = left
    @right = right
  end
  
  #SELECTORS
  def left()
    @left
  end
  
  def right()
    @right
  end
  

  #TYPEPREDS

  
  #CONVERSIONS
  def to_s
    'Union2d'+'['+(self.left.to_s)+','+(self.right.to_s)+']'
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
 def invariant?
    left.shape2d? and right.shape2d?
  end
  #typepreds
  def union2d?()
  self == Union2d
  end
  def shape1d?() false end
  def shape2d?() true end

  
 
    #operations
  #hilfsfunktion für graph_equal?
  def graph_equal_?(o2)
    (self.left.graph_equal?(o2.left) and self.right.graph_equal?(o2.right))
  end

  #prüft, ob 2 objekte deckungsgleich sind
  #Union2d#graph_equal_trans? ::= Shape x Point ->? Bool
      def graph_equal_trans?(o2)
    check_pre((o2.shape2d?))
   to1 = self.translate(Point2d[Point1d[(o2.bounds().range_x.first.coord - self.bounds().range_x.first.coord)], Point1d[(o2.bounds().range_y.first.coord - self.bounds().range_y.first.coord)]])   
   to1.graph_equal?(o2)
  end
 #translatierung einer 2d shape
 #Union2d#translate2d ::= shape,point :: Shape2d x Point2d -> Shape2d
  def translate2d(point)
    check_pre((point.point2d?))
    Union2d[self.left.translate2d(point), self.right.translate2d(point)]
  end
#translatierung allgemein
#Union2d#translate ::= (shape,point) :: Shape x Point ->? Range1d|Range2d
  def translate(point)
check_pre((point.point?))
self.translate2d(point)

end 

  

#prüft, ob ein Punkt in einer Shape enthalten ist
#Union2d#in? ::= shape,point :: Shape x Point ->? Bool
   def in?(point)
      check_pre((point.point2d?))
      (self.left.in?(point) or self.right.in?(point))
      end
      
  

end
  
